Nuprl Definition : rationals 11,40

rationals == quotient(b-union(; (:  int_nzero)); r,s.(qeq(rs) = tt)) 
latex



clarification:

rationals == quotient(b-union(; (:  int_nzero)); r,s.(qeq(rs) = tt  )) 
latex


Definitionstt, qeq(rs), , s = t, int_nzero, , x:A  B(x), b-union(AB), quotient(Ax,y.B(x;y))
FDL editor aliasesrationals

origin